a,b:rationals. (a + b) = (b + a)  rationals 

latex

Definitions	imon{i:l}, t  T, iabmonoid{i:l}, t.2, t.1, prop{i:l}, P  Q, mon{i:l}, grp{i:l}, abgrp{i:l}, qadd_grp, grp_op(g), x f y, grp_car(g), x:A. B(x)
Lemmas	abgrp wf, comm wf, grp id wf, grp op wf, grp car wf, monoid p wf, qadd grp wf, abmonoid comm